E:Type, T,V:(IdIdType), M:(IdLnkIdType), pred?:(E(?E)), info:(E((:Id  Id) + (:(:IdLnk
E:Type, T,V:(IdIdType), M:(IdLnkIdType), pred?:(E(?E)), info:(E( E)  Id))),
init:(i:IdEState((T(i)))), Trans:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))
init:(i:IdEState((T(i)))), Trans:(EState((T(i)))EState((T(i)))),
val:(e:Ekindcase(kind(e); a.(V(loc(e),a)); l,t.(M(l,t)))), time:(Erationals).
(e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 SWellFounded(pred!(e;e'))
 (e:E. 
 when-after(e;info;pred?;init;Trans;val;time)
  (:EState((T(loc(e))))  EState((T(loc(e)))))) 

latex

Definitions

{x:A| B(x)} , x:AB(x), a < b, void, False, A, , x:A. B(x), SWellFounded(R(x;y)), Type, Id, IdLnk, Unit, left + right, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t)), Knd, kind(e), rationals, pred(e), s = t, prop{i:l}, first(e), b, pred!(e;e'), ge(i; j), #$n, -n, n + m, n - m, f(a), when-after(e;info;pred?;init;Trans;val;time), loc(e), EState(T), x:A  B(x), t  T, A  B, P  Q, x:A. B(x), , b, , P  Q, P  Q, x.A(x), s+r, <a, b>, let x = a in b(x), sender(e), rcv?(e), A c B, P  Q, r - s, guard(T), sq_type(T), sqequal(s; t), atom{$n:n}

Lemmas

Id sq, qsub wf, rcv? wf, sender wf, es-shift wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, ge wf, nat properties, strongwellfounded wf, pred! wf, not wf, assert wf, first wf, pred wf, rationals wf, kind wf, loc wf, Knd wf, kindcase wf, EState wf, unit wf, IdLnk wf, Id wf, le wf, nat wf